nLab structural set theory

Contents

Context

Foundations

Idea
Examples

Elementary theory of the category of sets (ETCS)
Sets, Elements and Relations (SEAR)
Structural ZFC
Local set theory
Setoids
Homotopy-sets in homotopy type theory

Related Pages
References

Idea

A structural set theory is a set theory which describes structural mathematics, and only structural mathematics: Sets are conceived as objects that have elements, and are related to each other by functions or relations. In the most common structural set theories such as ETCS, sets are characterized by the functions between them, i.e. by the category (“Set”) which they form (Lawvere 65). This is what essentially all the application of set theory in the practice of mathematics actually uses – a point amplified by the approach of the introductory textbook Lawvere-Rosebrugh 03.

This is in contrast to traditional material set theory (cf material versus structural) such as ZFC or ZFA, where sets are characterized by the membership relation “ $\in$ ” and propositional equality of sets “ $=$ ” alone, and where sets can be elements of other sets, hence where there are sequences of sets which are elements of the next set in the sequence. This latter feature, however, is almost never actually used or even considered in mathematics, away from the study of material set theory itself.

As conceived by the structuralist, mathematics is the study of structures whose form is independent of the particular attributes of the things that make them up. For instance, in ZF set theory, “the set of natural numbers” can be defined as the von Neumann naturals $\omega_N = \{ \emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}, \dots \}$ or alternately as the Zermelo naturals $\omega_Z = \{ \emptyset, \{\emptyset\}, \{\{\emptyset\}\}, \dots \}$ , but either definition has all the necessary properties (namely, the properties making it a natural numbers object in the category of sets, when equipped with an appropriate successor operation). See, for instance, Benacerraf’s paper.

The structuralist says, essentially, that the number “ $3$ ” should denote “the third place in a natural numbers object” rather than some particular set such as $\{\emptyset, \{\emptyset\}, \{\emptyset, \{\emptyset\}\}\}$ as it does in any definition of “the set of natural numbers” in ZF.

Structural set theory provides a foundation of mathematics which is free of this “superfluous baggage” attendant on theories such as ZF, in which there is lots of information such as whether or not $3\in 17$ (yes, says von Neumann; no, says Zermelo) which is never used in mathematics. In a structural set theory, the elements (such as $3$ ) of a set (such as $\mathbb{N}$ ) have no identity apart from their existence as elements of that set, and whatever structure is given to that set by the functions and relations placed upon it. That is, sets (together with other attendant concepts such as elements, functions, and relations) are the “raw material” from which mathematical structures are built. By contrast, theories such as ZF may be called material set theories or membership-based set theories.

Thus, somewhat paradoxically, it turns out that one of the primary attributes of a structural set theory is that the elements of a set have no “internal” structure; they are only given structure by means of functions and relations. In particular, they are not themselves sets, and by default cannot be elements of any other set (not in the sense that it is false that they are, but in the sense that it is meaningless to ask whether they are), so that elements of different sets cannot be compared (unless and until extra structure is imposed). Structural set theory thus looks very much like type theory. We contrast it with material set theories such as ZF, in which the elements of sets can have internal structure, and are often (perhaps always) themselves sets.

Structural set theories can be distinguished by whether they include a formal notion of family of sets. Those that do are known as first-order set theories, while those that do not are known as zeroth-order set theories?. Higher-order set theories? have a notion of families of families in addition to families of sets. This parallels logic, where the role of propositions is played by sets and the role of predicates is played by families. Many structural set theories are only zeroth-order set theories, but the hSets and functions from hSets to the type hSet in homotopy type theory form a higher-order set theory.

It is hard to say precisely what makes a set theory “structural”, but one attempt is the notion of a structurally presented set theory.

Examples

Elementary theory of the category of sets (ETCS)

The original, and most commonly cited, categorially presented structural set theory is the elementary theory of the category of sets, or ETCS for short (Lawvere 65).

Therefore structural set theory is also called categorial set theory.

ETCS axiomatizes the category Set of sets as a well-pointed topos and thus lends itself to foundations of mathematics in topos theory. As such this is similar to the h-set-theory found in homotopy type theory (below), which forms a ΠW-pretopos.

ETCS is weaker than ZFC. To handle some esoteric parts of modern mathematics such as Borel determinacy, it must be supplemented with an axiom of collection, although it suffices for most everyday uses.

McLarty 93 argues that ETCS resolves the issues originally raised by Benacerraf 65.

Sets, Elements and Relations (SEAR)

Another structural set theory, which is stronger than ETCS (since it includes the axiom of collection by default) and also less closely tied to category theory, is SEAR.

Structural ZFC

One could reformulate ZFC as a three-sorted or dependently sorted structural set theory consisting of sets, elements, functions, and structural versions of the 10 standard ZFC axioms. This set theory is called structural ZFC.

It should also be possible to create an allegorical version of ZFC, but nobody has done so yet.

Local set theory

Local set theory avoids the use of any global universe but instead is formulated in a many-sorted language that has various forms of sorts including, for each sort a power-sort; see Bell and Aczel.

Setoids

Set theory set up in extensional intuitionistic type theory via setoids is structural.

Homotopy-sets in homotopy type theory

The collection of h-sets in homotopy type theory constitute a ΠW-pretopos, hence a structural set theory (Rijke-Spitters 13). If the type theory also has a type of all propositions, then the collections of h-sets constitute an elementary topos.

References

A textbook that introduces the foundations of mathematics informally via structural set theory is

William Lawvere, Robert Rosebrugh, Sets for Mathematics, Cambridge UP 2003.

The formal account of ETCS originates with

William Lawvere, An elementary theory of the category of sets, Proceedings of the National Academy of Science of the U.S.A 52 pp.1506-1511 (1965). (pdf)

Structural set theory found in homotopy type theory is discussed in

Egbert Rijke, Bas Spitters, Sets in homotopy type theory, Mathematical Structures in Computer Science, Volume 25, Issue 5 (From type theory and homotopy theory to Univalent Foundations of Mathematics) (arXiv:1305.3835)

which became one chapter in

Univalent Foundations Project, Homotopy Type Theory – Univalent Foundations of Mathematics

Relation to material set theory is discussed in

Michael Shulman, Comparing material and structural set theories (arXiv:1808.05204)